package gov.nasa.jpf.symbc.modelcounter.latte;

import java.util.HashMap;
import java.util.Map;
import java.util.Stack;

import sun.reflect.ReflectionFactory.GetReflectionFactoryAction;

import gov.nasa.jpf.symbc.numeric.BinaryLinearIntegerExpression;
import gov.nasa.jpf.symbc.numeric.Comparator;
import gov.nasa.jpf.symbc.numeric.Constraint;
import gov.nasa.jpf.symbc.numeric.ConstraintExpressionVisitor;
import gov.nasa.jpf.symbc.numeric.Expression;
import gov.nasa.jpf.symbc.numeric.IntegerConstant;
import gov.nasa.jpf.symbc.numeric.IntegerExpression;
import gov.nasa.jpf.symbc.numeric.LinearIntegerConstraint;
import gov.nasa.jpf.symbc.numeric.Operator;
import gov.nasa.jpf.symbc.numeric.SymbolicInteger;

/**
 * A visitor that constructs a simplified version of the constraint/expression
 * it is traversing. It turns constraints into canonical constraints, and
 * expressions into canonical expressions.
 * 
 * A constraint is canonical if and only if
 * 
 * <ul>
 * <li>its left-hand side is a canonical expression, and</li>
 * <li>its right-hand side is an {@link IntegerConstant}.</li>
 * </ul>
 * 
 * An expression is canonical if and only if either
 * 
 * <ul>
 * <li>it is an {@link IntegerConstant}, or</li>
 * <li>it is a {@link BinaryLinearIntegerExpression}, its operator is addition,
 * its left-hand side is a canonical sum, and its right-hand side is an
 * {@link IntegerConstant}.</li>
 * </ul>
 * 
 * A sum is canonical if and only if either
 * 
 * <ul>
 * <li>it is a canonical factor, or</li>
 * <li>it is a {@link BinaryLinearIntegerExpression}, its operator is addition,
 * its left-hand side is a canonical sum, and its right-hand side is a canonical
 * factor.</li>
 * </ul>
 * 
 * Lastly, a factor is canonical if and only if
 * 
 * <ul>
 * <li>it is a {@link BinaryLinearIntegerExpression},</li>
 * <li>its operator is multiplication,</li>
 * <li>its left-hand side is an {@link IntegerConstant}, and</li>
 * <li>its right-hand side is a {@link SymbolicInteger}.</li>
 * </ul>
 * 
 * To put it more concisely:
 * 
 * <pre>
 * CC ::= CE cmp IC
 * CE ::= IC | CS + IC
 * CS ::= CF | CS + CF
 * CF ::= IC * SI
 * </pre>
 * 
 * where {@code CC} stands for canonical constraint, {@code CE} for canonical
 * expression, {@code CS} for canonical sum, {@code CF} for canonical factor,
 * {@code IC} for integer constant, and {@code SI} for symbolic integer. Also,
 * {@code cmp} is one of {{@link Comparator#NE}, {@link Comparator#NE},
 * {@link Comparator#LT}, {@link Comparator#LE}, {@link Comparator#GT},
 * {@link Comparator#GE} .
 * 
 * @author Jaco Geldenhuys
 */
public class CanonizingVisitor extends ConstraintExpressionVisitor {

	/**
	 * The final, simplified constraint.
	 */
	private Constraint simple;

	/**
	 * A stack where temporary, simplified operands are stored during the
	 * traversal.
	 */
	private final Stack<IntegerExpression> stack;

	/**
	 * Flag to indicate whether or not an unsupported expression has been
	 * encountered during the traversal. If so, the visitor goes into an "idle"
	 * work where no work is performed.
	 */
	private boolean unsupportedOp;

	/**
	 * Flag that indicates that a conjunct is false and, therefore, the entire path condition is unsatisfiable.
	 */
	private boolean unsatisfiable;

	/**
	 * A representation of the integer constant "0".
	 */
	private final IntegerConstant zero;

	/**
	 * A representation of the integer constant "1".
	 */
	private final IntegerConstant one;

	/**
	 * The variable renaming visitor that is used by the canonizing visitor.
	 */
	private final RenamingVisitor renamer;

	/**
	 * The variable simple view visitor that is used by the canonizing visitor.
	 */
	private final SimpleViewVisitor viewer;

	/**
	 * Prepare the visitor's fields.
	 */
	public CanonizingVisitor() {
		simple = null;
		stack = new Stack<IntegerExpression>();
		unsupportedOp = false;
		unsatisfiable = false;
		zero = new IntegerConstant(0);
		one = new IntegerConstant(1);
		renamer = new RenamingVisitor();
		viewer = new SimpleViewVisitor();
	}

	/**
	 * Reset the visitor to prepare for a new traversal.
	 */
	public void reset() {
		simple = null;
		unsupportedOp = false;
		viewer.reset();
	}

	/**
	 * Reset the visitor for a new path condition.
	 */
	public void resetMap() {
		renamer.reset();
		unsatisfiable = false;
	}

	public boolean isUnsatisfiable() {
		return unsatisfiable;
	}

	/**
	 * Return the simplified view calculated by the visitor during its
	 * last traversal. If an unsupported expression was encountered, this
	 * function will return the string {@code "?"}.
	 * 
	 * @return the simplified view
	 */
	public String getConstraint() {
		if (simple != null) {
			simple.accept(renamer);
			Constraint s = renamer.getRenamedConstraint();
			s.accept(viewer);
			return viewer.toString();
		} else {
			return null;
		}
	}

	@Override
	public void postVisit(Constraint constraint) {
		if (unsupportedOp) {
			return;
		}
		IntegerExpression r = stack.pop();
		IntegerExpression l = stack.pop();
		Expression e = mergeCE(Operator.MINUS, l, r);
		if (e instanceof IntegerConstant) {
			// This is interesting: the constraint boils down to "k op 0" for
			// some constant k. Oh well, ...
			l = (IntegerConstant) e;
			r = new IntegerConstant(0);
		} else {
			assert e instanceof BinaryLinearIntegerExpression;
			BinaryLinearIntegerExpression f = (BinaryLinearIntegerExpression) e;
			l = makeCE(f.getLeft(), zero);
			r = new IntegerConstant(-(((IntegerConstant) f.getRight()).value()));
		}
		simple = removeZeros(new LinearIntegerConstraint(l, constraint.getComparator(), r));
	}

	private Constraint removeZeros(Constraint constraint) {
		Comparator op = constraint.getComparator();
		IntegerExpression l = (IntegerExpression) constraint.getLeft();
		IntegerConstant r = (IntegerConstant) constraint.getRight();
		BinaryLinearIntegerExpression le = null;
		IntegerConstant lc;
		if (l instanceof BinaryLinearIntegerExpression) {
			le = removeZeros((BinaryLinearIntegerExpression) ((BinaryLinearIntegerExpression) l).getLeft());
			lc = (IntegerConstant) ((BinaryLinearIntegerExpression) l).getRight();
		} else {
			lc = (IntegerConstant) l;
		}
		if (le == null) {
			boolean result = false;
			switch (constraint.getComparator()) {
			case NE:
				result = lc.value != r.value;
				break;
			case EQ:
				result = lc.value == r.value;
				break;
			case LT:
				result = lc.value < r.value;
				break;
			case LE:
				result = lc.value <= r.value;
				break;
			case GT:
				result = lc.value > r.value;
				break;
			case GE:
				result = lc.value >= r.value;
				break;
			}
			if (!result) {
				unsatisfiable = true;
			}
			return null;
		} else {
			IntegerExpression firstCoeff = le;
			while (firstCoeff instanceof BinaryLinearIntegerExpression) {
				firstCoeff = ((BinaryLinearIntegerExpression) firstCoeff).getLeft();
			}
			IntegerConstant coeff = (IntegerConstant) firstCoeff;
			if (coeff.value < 0) {
				le = scaleCS(-1, le);
				lc = scaleIC(-1, lc);
				r = scaleIC(-1, r);
				if (op == Comparator.LT) {
					op = Comparator.GT;
				} else if (op == Comparator.LE) {
					op = Comparator.GE;
				} else if (op == Comparator.GT) {
					op = Comparator.LT;
				} else if (op == Comparator.GE) {
					op = Comparator.LE;
				}
			}
			if (lc.value != 0) {
				le = new BinaryLinearIntegerExpression(le, Operator.PLUS, lc);
			}
		}
		return new LinearIntegerConstraint(le, op, r);
	}

	private BinaryLinearIntegerExpression removeZeros(
			BinaryLinearIntegerExpression expr) {
		if (expr.getOp() == Operator.MUL) {
			IntegerConstant c = (IntegerConstant) ((BinaryLinearIntegerExpression) expr).getLeft();
			return (c.value == 0) ? null : expr;
		} else {
			BinaryLinearIntegerExpression e = (BinaryLinearIntegerExpression) expr;
			BinaryLinearIntegerExpression l = removeZeros((BinaryLinearIntegerExpression) e.getLeft());
			BinaryLinearIntegerExpression r = (BinaryLinearIntegerExpression) e.getRight();
			IntegerConstant c = (IntegerConstant) r.getLeft();
			if (c.value == 0) {
				return l;
			} else if (l == null) {
				return r;
			} else {
				return new BinaryLinearIntegerExpression(l, Operator.PLUS, r);
			}
		}
	}

	@Override
	public void postVisit(BinaryLinearIntegerExpression expr) {
		if (unsupportedOp) {
			return;
		}
		IntegerExpression r = stack.pop(); // CE = IC | CS + IC
		IntegerExpression l = stack.pop(); // CE = IC | CS + IC
		switch (expr.getOp()) {
		case PLUS:
			stack.push(mergeCE(Operator.PLUS, l, r));
			break;
		case MINUS:
			stack.push(mergeCE(Operator.MINUS, l, r));
			break;
		case MUL:
			if (l instanceof IntegerConstant) {
				int lk = ((IntegerConstant) l).value();
				if (r instanceof IntegerConstant) {
					// Case 1: IC * IC
					int rk = ((IntegerConstant) r).value();
					stack.push(new IntegerConstant(lk * rk));
				} else {
					// Case 2: IC * (CS + IC)
					assert r instanceof BinaryLinearIntegerExpression;
					stack.push(scaleCE(lk, r));
				}
			} else {
				BinaryLinearIntegerExpression ll = (BinaryLinearIntegerExpression) l;
				if (r instanceof IntegerConstant) {
					// Case 3: (CS + IC) * IC
					int rk = ((IntegerConstant) r).value();
					stack.push(scaleCE(rk, ll));
				} else {
					// Case 4: (CS + IC) * (CS + IC)
					assert r instanceof BinaryLinearIntegerExpression;
					stack.clear();
					unsupportedOp = true;
				}
			}
			break;
		default:
			// Unsupported operation
			stack.clear();
			unsupportedOp = true;
			break;
		}
	}

	/**
	 * Visit an integer constant by placing -- on the stack -- a canonical
	 * expression that represents the integer value.
	 * 
	 * @see gov.nasa.jpf.symbc.numeric.ConstraintExpressionVisitor#postVisit(gov.nasa.jpf.symbc.numeric.IntegerConstant)
	 */
	@Override
	public void postVisit(IntegerConstant expr) {
		if (unsupportedOp) {
			return;
		}
		stack.push(expr);
	}

	/**
	 * Visit a symbolic integer by placing -- on the stack -- a canonical factor
	 * to represent the symbolic variable.
	 * 
	 * @see gov.nasa.jpf.symbc.numeric.ConstraintExpressionVisitor#postVisit(gov.nasa.jpf.symbc.numeric.SymbolicInteger)
	 */
	@Override
	public void postVisit(SymbolicInteger expr) {
		if (unsupportedOp) {
			return;
		}
		BinaryLinearIntegerExpression cs = makeCF(one, expr);
		stack.push(makeCE(cs, zero));
	}

	/**
	 * Merge two canonical expressions based on the given operator (which is
	 * either {@link Operator#PLUS} or {@link Operator#MINUS}).
	 * 
	 * @param op
	 *            the operator (either '+' or '-')
	 * @param left
	 *            the left-hand canonical expression
	 * @param right
	 *            the right-hand canonical expression
	 * @return the sum/difference of the canonical expressions again as a
	 *         canonical expression
	 */
	private IntegerExpression mergeCE(Operator op, Expression left,
			Expression right) {
		if (left instanceof IntegerConstant) {
			if (right instanceof IntegerConstant) {
				// Case 1: left = IC, right = IC
				return applyOp(op, left, right);
			} else {
				// Case 2: left = IC, right = CS + IC
				BinaryLinearIntegerExpression r = (BinaryLinearIntegerExpression) right;
				IntegerConstant c = applyOp(op, left, r.getRight());
				BinaryLinearIntegerExpression cs = (BinaryLinearIntegerExpression) r
						.getLeft();
				if (op == Operator.MINUS) {
					cs = scaleCS(-1, cs);
				}
				return makeCE(cs, c);
			}
		} else {
			BinaryLinearIntegerExpression l = (BinaryLinearIntegerExpression) left;
			if (right instanceof IntegerConstant) {
				// Case 3: left = CS + IC, right = IC
				IntegerConstant c = applyOp(op, l.getRight(), right);
				return makeCE(l.getLeft(), c);
			} else {
				// Case 4: left = CS + IC, right = CS + IC
				BinaryLinearIntegerExpression r = (BinaryLinearIntegerExpression) right;
				IntegerConstant c = applyOp(op, l.getRight(), r.getRight());
				BinaryLinearIntegerExpression ll = (BinaryLinearIntegerExpression) l
						.getLeft();
				BinaryLinearIntegerExpression rl = (BinaryLinearIntegerExpression) r
						.getLeft();
				return makeCE(mergeCS(op, ll, rl), c);
			}
		}
	}

	/**
	 * Merge two canonical sums (which may contain common symbolic integers)
	 * based on the given operator (which is either {@link Operator#PLUS} or
	 * {@link Operator#MINUS}).
	 * 
	 * @param op
	 *            the operator (either '+' or '-')
	 * @param left
	 *            the left-hand canonical sum
	 * @param right
	 *            the right-hand canonical sum
	 * @return the sum/difference of the canonical sums again as a canonical sum
	 */
	private BinaryLinearIntegerExpression mergeCS(Operator op,
			BinaryLinearIntegerExpression left,
			BinaryLinearIntegerExpression right) {
		if (op == Operator.MINUS) {
			return mergeCS(Operator.PLUS, left, scaleCS(-1, right));
		}
		if (left.getOp() == Operator.MUL) {
			if (right.getOp() == Operator.MUL) {
				// Case 1: left = CF, right = CF
				return mergeCF(op, left, right);
			} else {
				// Case 2: left = CF, right = CS + CF
				SymbolicInteger v = (SymbolicInteger) left.getRight();
				BinaryLinearIntegerExpression l = (BinaryLinearIntegerExpression) right
						.getLeft();
				BinaryLinearIntegerExpression r = (BinaryLinearIntegerExpression) right
						.getRight();
				SymbolicInteger rv = (SymbolicInteger) r.getRight();
				if (v.hashCode() < rv.hashCode()) {
					return makeCS(mergeCS(op, left, l), r);
				} else if (v.hashCode() > rv.hashCode()) {
					return makeCS(right, left);
				} else {
					return makeCS(l, mergeCF(op, left, r));
				}
			}
		} else {
			assert left.getOp() == Operator.PLUS;
			if (right.getOp() == Operator.MUL) {
				// Case 3: left = CS + CF, right = CF
				SymbolicInteger v = (SymbolicInteger) right.getRight();
				BinaryLinearIntegerExpression l = (BinaryLinearIntegerExpression) left
						.getLeft();
				BinaryLinearIntegerExpression r = (BinaryLinearIntegerExpression) left
						.getRight();
				SymbolicInteger rv = (SymbolicInteger) r.getRight();
				if (v.hashCode() < rv.hashCode()) {
					return makeCS(mergeCS(op, l, right), r);
				} else if (v.hashCode() > rv.hashCode()) {
					return makeCS(left, right);
				} else {
					return makeCS(l, mergeCF(op, r, right));
				}
			} else {
				// Case 4: left = CS + CF, right = CS + CF
				assert right.getOp() == Operator.PLUS;
				BinaryLinearIntegerExpression ll = (BinaryLinearIntegerExpression) left
						.getLeft();
				BinaryLinearIntegerExpression lr = (BinaryLinearIntegerExpression) left
						.getRight();
				BinaryLinearIntegerExpression rl = (BinaryLinearIntegerExpression) right
						.getLeft();
				BinaryLinearIntegerExpression rr = (BinaryLinearIntegerExpression) right
						.getRight();
				BinaryLinearIntegerExpression llrl = mergeCS(op, ll, rl);
				SymbolicInteger lrv = (SymbolicInteger) lr.getRight();
				SymbolicInteger rrv = (SymbolicInteger) rr.getRight();
				if (lrv.hashCode() < rrv.hashCode()) {
					return makeCS(mergeCS(op, llrl, lr), rr);
				} else if (lrv.hashCode() < rrv.hashCode()) {
					return makeCS(mergeCS(op, llrl, rr), lr);
				} else {
					return makeCS(llrl, mergeCF(op, lr, rr));
				}
			}
		}
	}

	/**
	 * Merge two canonical factors (which may refer to the same symbolic
	 * integer) based on the given operator (which is either
	 * {@link Operator#PLUS} or {@link Operator#MINUS}).
	 * 
	 * @param op
	 *            the operator (either '+' or '-')
	 * @param left
	 *            the left-hand canonical factor
	 * @param right
	 *            the right-hand canonical factor
	 * @return the sum/difference of the canonical factors again as a canonical
	 *         factor
	 */
	private BinaryLinearIntegerExpression mergeCF(Operator op,
			BinaryLinearIntegerExpression left,
			BinaryLinearIntegerExpression right) {
		SymbolicInteger lv = (SymbolicInteger) left.getRight();
		SymbolicInteger rv = (SymbolicInteger) right.getRight();
		if (lv.hashCode() < rv.hashCode()) {
			return makeCS(left, right);
		} else if (lv.hashCode() > rv.hashCode()) {
			return makeCS(right, left);
		} else {
			return makeCF(applyOp(op, left.getLeft(), right.getLeft()), lv);
		}

	}

	/**
	 * Apply the operator (which is either {@link Operator#PLUS} or
	 * {@link Operator#MINUS}) to the supplied integer parameters and return the
	 * result as an {@link IntegerConstant}.
	 * 
	 * @param op
	 *            the operator (either '+' or '-')
	 * @param left
	 *            the first integer operand
	 * @param right
	 *            the second integer operand
	 * @return an integer constant that represents the sum/difference of the
	 *         operands
	 */
	private IntegerConstant applyOp(Operator op, int left, int right) {
		if (op == Operator.PLUS) {
			return new IntegerConstant(left + right);
		} else {
			assert op == Operator.MINUS;
			return new IntegerConstant(left - right);
		}
	}

	/**
	 * Apply the operator (which is either {@link Operator#PLUS} or
	 * {@link Operator#MINUS}) to the supplied integer parameters (supplied as
	 * instances of {@link Expression} but guaranteed to be instances of
	 * {@link IntegerConstant}) and return the result as an
	 * {@link IntegerConstant}.
	 * 
	 * @param op
	 *            the operator (either '+' or '-')
	 * @param left
	 *            the first integer operand as an {@link Expression}
	 * @param right
	 *            the second integer operand as an {@link Expression}
	 * @return an integer constant that represents the sum/difference of the
	 *         operands
	 */
	private IntegerConstant applyOp(Operator op, Expression left,
			Expression right) {
		return applyOp(op, ((IntegerConstant) left).value(),
				((IntegerConstant) right).value());
	}

	/**
	 * Given a canonical expression and a scaling factor, produce a new
	 * canonical expression where the constant values have all been scaled by
	 * the factor. For example, given a scaling factor of 5 and the canonical
	 * expression
	 * 
	 * <pre>
	 * (-1 * x) + (2 * y) + (-3 * z) + 9
	 * </pre>
	 * 
	 * the function returns the canonical expression
	 * 
	 * <pre>
	 * (-5 * x) + (10 * y) + (-15 * z) + 45
	 * </pre>
	 * 
	 * @param factor
	 *            the factor to scale by
	 * @param ce
	 *            the canonical expression
	 * @return a new, scaled canonical expression
	 */
	private IntegerExpression scaleCE(int factor, IntegerExpression ce) {
		if (ce instanceof IntegerConstant) {
			return scaleIC(factor, ce);
		} else {
			BinaryLinearIntegerExpression e = (BinaryLinearIntegerExpression) ce;
			BinaryLinearIntegerExpression cs = scaleCS(factor,
					(BinaryLinearIntegerExpression) e.getLeft());
			IntegerConstant v = scaleIC(factor, e.getRight());
			return makeCE(cs, v);
		}
	}

	/**
	 * Given a canonical sum and a scaling factor, produce a new canonical sum
	 * whose constant values have all been scaled by the factor. For example,
	 * given a scaling factor of -2 and the canonical sum
	 * 
	 * <pre>
	 * (1 * x) + (-3 * y) + (2 * z)
	 * </pre>
	 * 
	 * the function returns the canonical sum
	 * 
	 * <pre>
	 * (-2 * x) + (6 * y) + (-4 * z)
	 * </pre>
	 * 
	 * @param factor
	 *            the factor to scale by
	 * @param cs
	 *            the canonical sum
	 * @return a new, scaled canonical sum
	 */
	private BinaryLinearIntegerExpression scaleCS(int factor,
			BinaryLinearIntegerExpression cs) {
		if (cs.getOp() == Operator.PLUS) {
			BinaryLinearIntegerExpression l = scaleCS(factor,
					(BinaryLinearIntegerExpression) cs.getLeft());
			BinaryLinearIntegerExpression r = scaleCF(factor,
					(BinaryLinearIntegerExpression) cs.getRight());
			return makeCS(l, r);
		} else {
			return scaleCF(factor, cs);
		}
	}

	/**
	 * Given a canonical factor and a scaling factor, produce a new canonical
	 * whose constant value has been scaled by the scaling factor.
	 * 
	 * @param factor
	 *            the factor to scale by
	 * @param cf
	 *            the canonical factor
	 * @return a new, scaled canonical factor
	 */
	private BinaryLinearIntegerExpression scaleCF(int factor,
			BinaryLinearIntegerExpression cf) {
		assert cf.getOp() == Operator.MUL;
		IntegerConstant l = (IntegerConstant) cf.getLeft();
		l = new IntegerConstant(factor * l.value());
		return makeCF(l, cf.getRight());
	}

	/**
	 * Given an {@link IntegerExpression} that is guaranteed to be an instance
	 * of an {@link IntegerConstant}, produce another integer constant that is
	 * equal to the given constant scaled by a factor.
	 * 
	 * @param factor
	 *            the factor to scale by
	 * @param expr
	 *            the integer expression
	 * @return a scaled integer constant
	 */
	private IntegerConstant scaleIC(int factor, IntegerExpression expr) {
		return new IntegerConstant(factor * ((IntegerConstant) expr).value());
	}

	/**
	 * Given a canonical sum and an {@link IntegerConstant}, construct a
	 * canonical expression.
	 * 
	 * @param cs
	 *            the canonical sum
	 * @param ic
	 *            the integer constant
	 * @return a canonical expression
	 */
	private IntegerExpression makeCE(IntegerExpression cs, IntegerConstant ic) {
		return new BinaryLinearIntegerExpression(cs, Operator.PLUS, ic);
	}

	/**
	 * Given a canonical sum and a canonical factor, combine them to form a new
	 * canonical sum. We assume that the symbolic integer of the given canonical
	 * factor is "greater than" all of the symbolic integers that appear in the
	 * given canonical sum.
	 * 
	 * @param cs
	 *            the canonical sum
	 * @param cf
	 *            the canonical factor
	 * @return a new canonical sum of the given sum and the factor
	 */
	private BinaryLinearIntegerExpression makeCS(
			BinaryLinearIntegerExpression cs, BinaryLinearIntegerExpression cf) {
		assert cf.getOp() == Operator.MUL;
		return new BinaryLinearIntegerExpression(cs, Operator.PLUS, cf);
	}

	/**
	 * Given an {@link IntegerConstant} and an {@link IntegerExpression} (that
	 * is guaranteed to be a {@link SymbolicInteger}), return a new canonical
	 * factor by construction the product of the constant and the symbolic
	 * variable.
	 * 
	 * @param ic
	 *            the integer constant
	 * @param si
	 *            the symbolic variable (integer)
	 * @return a canonical factor
	 */
	private BinaryLinearIntegerExpression makeCF(IntegerConstant ic,
			IntegerExpression si) {
		assert si instanceof SymbolicInteger;
		return new BinaryLinearIntegerExpression(ic, Operator.MUL, si);
	}

	/**
	 * A visitor that constructs a simplified string version of the constraint/expression
	 * it is traversing.
	 * 
	 * @author Jaco Geldenhuys
	 */
	private class SimpleViewVisitor extends ConstraintExpressionVisitor {

		/**
		 * The final, simplified string.
		 */
		private StringBuilder view;

		/**
		 * Flag to indicate whether or not an unsupported expression has been
		 * encountered during the traversal. If so, the visitor goes into an "idle"
		 * work where no work is performed.
		 */
		private boolean unsupportedOp;

		/**
		 * Prepare the visitor's fields.
		 */
		public SimpleViewVisitor() {
			view = new StringBuilder();
			unsupportedOp = false;
		}

		/**
		 * Reset the visitor to prepare for a new traversal.
		 */
		public void reset() {
			view.delete(0, view.length());
			unsupportedOp = false;
		}

		/**
		 * Return the simplified view calculated by the visitor during its
		 * last traversal. If an unsupported expression was encountered, this
		 * function will return the string {@code "?"}.
		 * 
		 * @return the simplified view
		 */
		@Override
		public String toString() {
			return view.toString().replaceAll(" ", "");
		}

		@Override
		public void postVisit(Constraint constraint) {
			if (unsupportedOp) {
				return;
			}
			view.append(constraint.getComparator().toString());
		}

		@Override
		public void postVisit(BinaryLinearIntegerExpression expr) {
			if (unsupportedOp) {
				return;
			}
			view.append(expr.getOp().toString());
		}

		@Override
		public void postVisit(IntegerConstant expr) {
			if (unsupportedOp) {
				return;
			}
			view.append(expr.toString().replaceAll("CONST_", ""));
//			view.append(';');
		}

		@Override
		public void postVisit(SymbolicInteger expr) {
			if (unsupportedOp) {
				return;
			}
			view.append(expr.toString());
//			view.append(';');
		}

	}

	/**
	 * A visitor that renames all the variables inside a constraint.
	 * 
	 * @author Jaco Geldenhuys
	 */
	private class RenamingVisitor extends ConstraintExpressionVisitor {

		/**
		 * The final, renamed constraint.
		 */
		private Constraint renamed;

		/**
		 * Mapping from symbolic integers to renamed symbolic integers.
		 */
		private Map<SymbolicInteger, SymbolicInteger> varMap;

		/**
		 * A stack where renamed operands are stored during the
		 * traversal.
		 */
		private final Stack<IntegerExpression> stack;

		/**
		 * Prepare the visitor's fields.
		 */
		public RenamingVisitor() {
			renamed = null;
			varMap = new HashMap<SymbolicInteger, SymbolicInteger>();
			stack = new Stack<IntegerExpression>();
		}

		public void reset() {
			varMap.clear();
		}

		/**
		 * Return the renamed constraint calculated by the visitor during its
		 * last traversal.
		 * 
		 * @return the renamed constraint
		 */
		public Constraint getRenamedConstraint() {
			return renamed;
		}

		@Override
		public void postVisit(Constraint constraint) {
			IntegerExpression r = stack.pop();
			IntegerExpression l = stack.pop();
			renamed = new LinearIntegerConstraint(l, constraint.getComparator(), r);
		}

		@Override
		public void postVisit(BinaryLinearIntegerExpression expr) {
			IntegerExpression r = stack.pop(); // CE = IC | CS + IC
			IntegerExpression l = stack.pop(); // CE = IC | CS + IC
			stack.push(new BinaryLinearIntegerExpression(l, expr.getOp(), r));
		}

		@Override
		public void postVisit(IntegerConstant expr) {
			stack.push(expr);
		}

		@Override
		public void postVisit(SymbolicInteger expr) {
			SymbolicInteger e = varMap.get(expr);
			if (e == null) {
				e = new SymbolicInteger("V" + varMap.size());
				varMap.put(expr, e);
			}
			stack.push(e);
		}

	}

}
